Add Erdős Problem 70 (3-uniform partition relation on the continuum)#3784
Add Erdős Problem 70 (3-uniform partition relation on the continuum)#3784henrykmichalewski wants to merge 5 commits intogoogle-deepmind:mainfrom
Conversation
Formalises Problem 70: the partition relation 𝔠 → (β, n)³₂ for triples, for every countable β and finite n. Introduces OrdinalCardinalRamsey3 using Set.Triplewise to generalise the 2-uniform partition relation to triples, states the main open theorem, records the Erdős-Rado partial variant, and proves a monotonicity lemma. Reference: https://www.erdosproblems.com/70 Assisted by Claude (Anthropic).
|
Closes #303 |
… docstring Insert canonical statement text + source URL from sage/conjecturing/sources/erdos_statements.json into the module docstring, matching the Round C pass on the private repo. The theorem statements and references are unchanged.
| @@ -0,0 +1,208 @@ | |||
| /- | |||
| Copyright 2025 The Formal Conjectures Authors. | |||
There was a problem hiding this comment.
nit: Could you update the copyright year to 2026 for this new file?
| -/ | ||
| @[category research open, AMS 3] | ||
| theorem erdos_70 : | ||
| answer(True) ↔ |
There was a problem hiding this comment.
Should this use answer(sorry) rather than answer(True)? The Erdős page marks the general relation open, so answer(True) makes the file record a solved positive answer.
| -/ | ||
| def OrdinalCardinalRamsey3 (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop := | ||
| -- For any partition of 3-element subsets into red and blue: | ||
| ∀ (isRed : α.ToType → α.ToType → α.ToType → Prop), |
There was a problem hiding this comment.
Should this be a coloring of unordered 3-element subsets rather than an arbitrary predicate on ordered triples? As written, isRed x y z need not be symmetric and can also be queried on repeated vertices. I would suggest quantifying over {s : Finset α.ToType // s.card = 3} or adding the symmetry and distinctness constraints explicitly.
Paul-Lez
added
the
awaiting-author
…k] + copyright 2026 Per Paul-Lez review on PR google-deepmind#3784. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (google-deepmind#3900).
|
@Paul-Lez — applied the mechanical nits in |
… (Paul-Lez review) Two fixes per Paul-Lez's review: - The coloring `isRed : α → α → α → Prop` was on ordered triples; the source partitions unordered 3-element subsets. Add an explicit symmetry constraint requiring `isRed` to be invariant under permutations of three distinct arguments. - The headline used `answer(True)`, but the general relation is OPEN on the Erdős page; switch to `answer(sorry)`.
|
Thanks for the review @PaulLez. Pushed b0a7ad0 on |
2 participants
Formalises Erdős Problem 70: the 3-uniform partition relation$\mathfrak{c} \to (\beta, n)^3_2$ for every countable ordinal $\beta$ and every finite $n$ .
Contents
OrdinalCardinalRamsey3: usesSet.Triplewiseto generalise the 2-uniform partition relation to triples.Assisted by Claude (Anthropic).